\begin{tabbing} $\forall$\=${\it es}$:ES, $T$:Type, ${\it eq}$:EqDecider($T$), $v$:$T$, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$T$)\} ,\+ \\[0ex]${\it e'}$:\{${\it e'}$:E$\mid$ $e$ $\leq$loc ${\it e'}$ \& ($x$ after ${\it e'}$) = $v$\} . \-\\[0ex]$\exists$${\it e'}$$\geq$$e$.($x$ after ${\it e'}$) = $v$ \& $\forall$${\it e''}$$\in$[$e$,${\it e'}$).$\neg$(($x$ after ${\it e''}$) = $v$) \end{tabbing}